import parse_input
import wtsn_solve_test01_smt
import draw_solution
import postprocess


if __name__ == "__main__":
    tasks,transaction_map,latency_bound = parse_input.json_parse("./inputs/example1.json")
    
    n_transactions = len(transaction_map)
    
    start_times,freqs = wtsn_solve_test01_smt.wtsn_smt_model(n_transactions,tasks,latency_bound)
    
    if start_times != None and freqs != None:
        #postprocess data
        postprocess.smt_postprocess(tasks,start_times,freqs)
        # draw the sheduling result of WTSN
        draw_solution.draw_combined_machine_timestamp_res(tasks,start_times,freqs,transaction_map)
        draw_solution.draw_timestamp_freq_res(tasks,start_times,freqs,transaction_map)
        
